package be.riaan.twelfdsl;
import collection.mutable.{Map,HashMap}

trait FreshMaker[From, To] {
  val existing: Map[From, To] = new HashMap[From, To]
  
  def make(i: Int): To
  
  def getOrMake(s: From): To = existing.get(s) match {
    case Some(l) => l
    case None => val l = make(existing.size); existing += s -> l
    l
  }
}

trait Twelfdsl {
  trait TwelfExpr
  
  def arg(e: TwelfExpr): String = " ("+e.toString+") "
  def brack(e: TwelfExpr): String = " ["+e.toString+"] "
  def arg_list(tp: String, el: List[TwelfExpr]): String = el match {
    case Nil => "nil_"+tp
    case x :: xs => arg("cons_"+tp+arg(x)+arg_list(tp, xs))
  }
  
  def arg_opt(tp: String, el: Option[TwelfExpr]): String = el match {
    case None => "none_"+tp
    case Some(x) => arg("some_"+tp+arg(x))
  }
    
  val vlabs = new FreshMaker[String, VLab] { def make(i: Int) = VLab(i) }
  val tlabs = new FreshMaker[String, TLab] { def make(i: Int) = TLab(i) }

  implicit def str2twelfexpr(s: String): TwelfExpr = new TwelfExpr() {override def toString=s}
  implicit def symbol2vlab(s: Symbol): VLab = vlabs.getOrMake(s.name)
  implicit def symbol2tlab(s: Symbol): TLab = tlabs.getOrMake(s.name)
  case class VLab(l: Int) extends TwelfExpr { override def toString = "vlab_nat "+int2peano(l) }
  case class TLab(l: Int) extends TwelfExpr { override def toString = "tlab_nat "+int2peano(l) }
  def int2peano(i: Int): String = i match { case 0 => "0" case i => "s"+arg(int2peano(i-1))}
  trait Tm extends TwelfExpr
  trait Tp extends TwelfExpr
  trait Member extends TwelfExpr
  trait Path extends TwelfExpr

  object __ extends Tm with Tp with Member with Path { override def toString = "_" }

  case class tmvar(name: String) extends Tm { override def toString = name }
  case class tmvarpath(name: String) extends Path { override def toString = name }
  
  case class let(vname: String, pname: String, tp: Tp, tm: Tm)(scope: Tm => Path => Tm) extends Tm {
    override def toString = "letv "+arg(tp)+arg(tm)+arg(brack(vname)+brack(pname)+scope(tmvar(vname))(tmvarpath(pname)))
  }
 
  case class letnew(vname: String, pname: String, tp: Tp)(scope: Tm => Path => Tm) extends Tm {
    override def toString = "letv "+arg(tp)+arg(nw(tp))+arg(brack(vname)+brack(pname)+scope(tmvar(vname))(tmvarpath(pname)))
  }
  
  case class nw(tp: Tp) extends Tm {
    override def toString = "new "+arg(tp)
  }
  
  case class fld(tgt: Tm, vl: VLab) extends Tm {
    override def toString = "field "+arg(tgt)+arg(vl)
  } 
  
  case class meth(tgt: Tm, vl: VLab, args: Tm*) extends Tm {
    override def toString = "meth "+arg(tgt)+arg(vl)+arg_list("tm", args.toList)
  } 
  
  case class unit() extends Tm {
    override def toString = "unit"
  } 
  
  case class Unit() extends Tp {
    override def toString = "Unit"
  } 

  case class tsel(tgt: Tm, dp: Path, tl: TLab) extends Tp {
    override def toString = "tsel "+arg(tgt)+arg(dp)+arg(tl)
  } 
  
  case class sng(tgt: Tm, dp: Path) extends Tp {
    override def toString = "single "+arg(tgt)+arg(dp)
  } 
  
  case class sig(selfname: String, parents: Tp*)(members: Tm => List[Member]) extends Tp {
    override def toString = "sig "+arg_list("tp", parents.toList)+arg(brack(selfname)+arg_list("mem", members(tmvar(selfname))))
  } 
  
  case class fdecl(vl: VLab, tp: Tp, tm: Option[Tm]) extends Member {
    override def toString = "fdecl "+arg(vl)+arg(tp)+arg_opt("tm", tm)
  }
  
  case class tpdecl(tl: TLab, tp: Option[Tp]) extends Member {
    override def toString = "tpdecl "+arg(tl)+arg_opt("tp", tp)
  }
  
  case class cdecl(tl: TLab, selfname: String, parents: Tp*)(members: Tm => List[Member])  extends Member {
    override def toString = "cdecl "+arg(tl)+arg_list("tp", parents.toList)+arg(brack(selfname)+arg_list("mem", members(tmvar(selfname))))
  }
  
  // TODO: mdecl
  
  case class path_new(tp: Tp) extends Path {
    override def toString = "path-new "+arg(tp)
  } 
  
  case class path_fsel(a: VLab, p: Path) extends Path {
    override def toString = "path-fsel "+arg(a)+arg(p)
  } 
  
}

object peano extends Twelfdsl with Application{
  val progtp: Tp = sig("thisprog") { thisprog => List(
      cdecl('Any, "this0"){ x => Nil })
  }
  
  val twelfsrc = letnew("prog", "pprog", progtp) { prog => pprog =>
    letnew("any", "pany", tsel(prog, pprog, 'Any)) { any => pany => unit }
  }
  
  Console.println(twelfsrc)
}
